package bcontractor.propositional.factories;

import java.util.ArrayList;
import java.util.HashMap;
import java.util.HashSet;
import java.util.List;
import java.util.Map;
import java.util.Set;

import bcontractor.propositional.PropositionalSentence;

/**
 * Implementação de problema aleatório, de acordo com alguns parâmetros. Gera
 * problemas com número definido de variáveis de cláusulas, usando sempre
 * cláusulas 3-SAT.
 * 
 * @author lundberg
 * 
 */
public class PropositionalProblemBuilder {

	private int nVariables;

	private Set<PropositionalSentence> clauses = new HashSet<PropositionalSentence>();

	private Set<Integer> missingAtoms = new HashSet<Integer>();

	private List<PropositionalSentence> clauseList = new ArrayList<PropositionalSentence>();

	private Map<Integer, Integer> atomCount = new HashMap<Integer, Integer>();

	public PropositionalProblemBuilder(int nVariables) {
		this.nVariables = nVariables;
		this.initializeAtomCount();
	}

	/**
	 * Inicializa a contagem de literais
	 * 
	 * @param atomCount
	 *            atomCount
	 */
	public void initializeAtomCount() {
		for (int atom = 1; atom <= nVariables; atom++) {
			atomCount.put(atom, 0);
			missingAtoms.add(atom);
		}
	}

	public int getNVariables() {
		return nVariables;
	}

	public int getNClauses() {
		return this.clauses.size();
	}

	public List<PropositionalSentence> getClauses() {
		return new ArrayList<PropositionalSentence>(this.clauseList);
	}

	/**
	 * Adiciona uma cláusula à fórmula, atualizando as estruturas de dados de
	 * controle.
	 * 
	 * @param clauses
	 *            clauses
	 * @param clauseList
	 *            clauseList
	 * @param atomCount
	 *            atomCount
	 * @param candidate
	 *            candidate
	 */
	public void add(PropositionalSentence candidate) {
		if (clauses.add(candidate)) {
			clauseList.add(candidate);
			for (Integer literal : candidate.getClauses()[0]) {
				Integer atom = Math.abs(literal);
				Integer count = atomCount.get(atom);
				atomCount.put(atom, count + 1);
				if (count == 0) {
					missingAtoms.remove(atom);
				}
			}
		}
	}

	/**
	 * Remove a cláusula da fórmula, atualizando as estrutudas de dados de
	 * controle.
	 * 
	 * @param clauses
	 *            clauses
	 * @param clauseList
	 *            clauseList
	 * @param atomCount
	 *            atomCount
	 * @param removed
	 *            removed
	 */
	public void remove(PropositionalSentence removed) {
		clauses.remove(removed);
		clauseList.remove(removed);
		for (Integer literal : removed.getClauses()[0]) {
			Integer atom = Math.abs(literal);
			Integer count = atomCount.get(atom);
			atomCount.put(atom, atomCount.get(atom) - 1);
			if (count == 1) {
				missingAtoms.add(atom);
			}
		}
	}

	/**
	 * Checks if the problem being built has missing atoms.
	 * 
	 * @return boolean
	 */
	public boolean hasMissingAtoms() {
		return !this.missingAtoms.isEmpty();
	}

	/**
	 * Obtains some of the current missing atoms
	 * 
	 * @return integer
	 */
	public Integer nextMissingAtom() {
		if (this.missingAtoms.isEmpty()) {
			throw new IllegalStateException("There is no missing atom.");
		}
		return this.missingAtoms.iterator().next();
	}

	/**
	 * Obtains the first clause, the oldest.
	 * 
	 * @return clause
	 */
	public PropositionalSentence getFirstClause() {
		return this.clauseList.get(0);
	}

	/**
	 * Checks if the given clause is already at the problem
	 * 
	 * @param clause
	 * @return boolean
	 */
	public boolean hasClause(PropositionalSentence clause) {
		return this.clauses.contains(clause);
	}
}
